D:Dsys, i:Id, m:M(i).Msg. mlnk(m)  IdLnk 

latex

Definitions	IdLnk, M(i), x:A. B(x), Id, Dsys, mlnk(m), M.Msg, Msg(da), Msg(M), t  T
Lemmas	dsys wf, Id wf, d-m wf, ma-msg wf